;;;lambda演算


TRUE := λx y.x
FLASE := λx y.y
AND := λp q.p q FALSE
OR := λp q.p q TRUE q
NOT := λp.p FALSE TRUE
IFTHENELSE := λp x y. p x y

;;AND计算演示推导
AND TRUR TRUE                   ;将TRUE和TRUE作用于AND
=λp q.p q FALSE (TRUE TRUE)     ;代换AND
=TRUE TRUE FALSE                ;将TRUE代换，将TRUE和FALSE应该于TRUE
=λx y.x TRUE FALSE              
=TRUE

CONS := λx y.λp IF p x y
CAR := λx.x TRUE
CDR := λx.x FALSE


;;CONS过程推导,返回一个过程
CONS m1 m2
=λx y.λp.IF p x y (m1 m2)
=λp.IF p m1 m2

;;CAR计算推导
CAR (IF p m1 m2)
=λx.(x TRUE) (λp.IF p m1 m2)
=(λp.IF p m1 m2) TRUE
=IF.TRUE m1 m2
=m1

;;;使用scheme进行编码
#lang racket
(define (cons1 x y)
  (define (dispatch m)
    (cond ((= m 0) x)
          ((= m 1) y)))
  dispatch)

(define (car1 z) (z 0))
(define (cdr1 z) (z 1))


;;或者
#lang racket
(define (cons1 x y)
  (lambda (m) (m x y)))
(define (car1 z)
  (z (lambda (p q) p)))
(define (cdr1 z)
  (z (lambda (p q) q)))
  
;;Y组合子
Y g= g(Y g)
Y=λf.(λx.f(x x)) (λx.f(x x))
Y g=(λf.(λx.f(x x)) (λx.f(x x))) g
   =(λx.g(x x))(λx.g(x x))            ;用λx.g(x x)替换x这个的变量                  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;                                   
   =g(λx.g(x x) λx.g(x x))            ;这两步将一直递归演算下去，永不停机            ;; =(λx.g(x x))(λx.g(x x)) ;;
   =g(Y g)                                                                      ;; =g(λx.g(x x) λx.g(x x)) ;;
                                                                                ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
   =g (λx.g (x x) λx.g (x x))
   =g (g (λx.g (x x) λx.g (x x)))
   =g (g (g (λx.g (x x) λx.g (x x))))
   =......

;;scheme进行编码
(define (Y f)
  ((lambda (u)
     (u u))
   (lambda (x)
     (f (lambda args
          (apply (x x) args))))))
 
((Y
  (lambda (fab)
    (lambda (n)
      (if (zero? n)
          1
          (* n (fab (- n 1)))))))
 10)
 
==>                         ;;将上面两个合并
(((lambda ()
    ((lambda (f)
       (f f))
     (lambda (x)
       ((lambda (y)
          (lambda (n)
            (if (zero? n)
                1
                (* n (y (- n 1)))))) (lambda z
                                       (apply (x x) z)))))))5)
